the_w:World, l:IdLnk, t:. snds(l;t)  Msg List 

latex

Definitions	snds(l;t), concat(ll), map(f;as), Msg, m(l;t), i  j < k, P & Q, AB, {i..j}, upto(n), x:A. B(x), , IdLnk, t  T, World
Lemmas	world wf, IdLnk wf, nat wf, upto wf, int seg wf, le wf, w-ml wf, map wf, w-Msg wf, concat wf